#pragma once


#include "vector"
#include "fstream"
#include "string"
using namespace std;
#include "LogicExpression.h"

class LogicExpression;
class VarExpression;
class FuncExpression;
class ListExpression;


class Substitute
{
	struct SubstitutePair
	{
		LogicExpression* oldExpr;
		LogicExpression* newExpr;
	};
private:
	bool flag;
	vector<SubstitutePair> listSubstitutePairs;
	static Substitute unifyVar(LogicExpression* var, LogicExpression* x, Substitute& s);
	
public:
	Substitute(bool _flag){	flag=_flag;};
	Substitute(){	flag=true;};
	bool isFalse(){return !flag;};
	void add(LogicExpression* oldExpr,LogicExpression* newExpr);
	static Substitute unify(LogicExpression* x, LogicExpression* y, Substitute& s);
	int find(LogicExpression* expr);
	LogicExpression* getNewExpressionAt(int index){return listSubstitutePairs[index].newExpr;};
	
};


class HornClause
{
private:	
	LogicExpression*  positiveLiteral;
	bool havePositiveLiteral;
public:
	bool ishavingPositiveLiteral(){return havePositiveLiteral;};
	HornClause(){havePositiveLiteral=false;};
	 vector<LogicExpression*> negativeLiterals;
	 void setPositiveLiteral(LogicExpression*  _positiveLiteral)
	 { 
		 positiveLiteral = _positiveLiteral ; 
		 havePositiveLiteral=true;
	 };
	 LogicExpression* getPositiveLiteral(){return positiveLiteral;};


};

class RobotLogic
{
private:
	vector<HornClause> KB;
	vector<LogicExpression*> singleExpressions;
	vector<LogicExpression*> string2ListExpressions(string str);
	LogicExpression* string2Expression(string str);
public:
	void loadKB(char* fileName);
	bool FOL_FC_Ask(LogicExpression* alpha);
	bool FOL_FC_Ask(string alphaString);
	void addSingleExpression(LogicExpression*);
	void addSingleExpression(string exprString);
	RobotLogic(void);
	~RobotLogic(void);
};


